Definitions | Prop, t T, M(i), P & Q, A B, Feasible(D), A || B, P  Q, x:A. B(x), interface-link(A;B;l;tg), P  Q, P  Q,  x. t(x), x(s), false , true , i< j,  b, tl(l), i j, if b t else f fi, nth_tl(n;as), hd(l), Y, False, A, A B, l[i], ||as||, A & B, , (x l), x:A. B(x), ( x L.P(x)), interface-compatible(A;B), b, P Q |